COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	SLIDES FOR CIRCUMSCRIPTION LECTURE - May 10, 1978
C00003 00003	okmove(x,l,s) ⊃ at(x,l,result(move(x,l),s))
C00004 ENDMK
C⊗;
SLIDES FOR CIRCUMSCRIPTION LECTURE - May 10, 1978

Suppose we know of just two individuals a and b.

P(a) ∧ P(b) ⊃ ∀x.P(x)

∀x.(P(x) ≡ x=a ∨ x=b)

(a=a ∨ a=b) ∧ (b=a ∨ b=b) ⊃ ∀x.(x=a ∨ x=b)

This is killing a fly with a sledge hammer.

P(a) ∧ P(b) ∧ ∀xy.(P(x,y) ⊃ P(f(x,y))) ⊃ ∀x.(Q(x) ⊃ P(x))

gets us

Q(a) ∧ Q(b) ∧ Q(f(a,a)) ∧ Q(f(b,b)) ∧ Q(f(a,b)) ∧ Q(f(b,a)) ∧ Q(f(a,f(b,a))) ∧ etc.



P(0) ∧ ∀n.(P(n) ⊃ P(n+1)) ⊃ ∀n.(integer n ⊃ P(n))

THE THINGS I KNOW ABOUT ARE ALL THAT IS RELEVANT.

okmove(x,l,s) ⊃ at(x,l,result(move(x,l),s))